Parallelize & Partition Verification #229
Conversation
|
Note to reviewers: I would recommend reading the logs for each job to get a better idea of how the parallelization works--I tried to be fairly liberal with debug output. |
|
Note: once this is approved by a second reviewer, I'll go ahead and change our settings to require the Verify std library (partition) jobs instead of the regular Verify std library ones. The |
Perhaps that's an issue we should just address in Kani? For example, when thread pools are enabled, print a thread id as prefix to each line of output? |
carolynzech
changed the title
kani -j with no arguments defaults to the number of CPUs, so no need for a fixed number
Edit: implemented in #3790 |
This harness takes between 22-25 minutes in CI. Change the harnesses's macro to use kissat solver instead, which brings verification time down to ~7 seconds. As an aside, I noticed this problem because the partition 1 runner in #229 is taking ~55 minutes, where the other partitions are taking ~30 minutes. This harness accounts for almost the entire difference. One nice consequence of partitioning verification is that it will make performance issues like this more noticeable. By submitting this pull request, I confirm that my contribution is made under the terms of the Apache 2.0 and MIT licenses.
Fix a typo introduced in #229 that prevents `kani-args` from getting passed to the `kani` command. This was discovered by @tengjiang (see #231). By submitting this pull request, I confirm that my contribution is made under the terms of the Apache 2.0 and MIT licenses.
Shard Kani verification workflow across multiple runners by:
kani list --format json, which outputs a JSON file like this:{ "kani-version": "0.56.0", "file-version": "0.1", "standard-harnesses": { "src/lib.rs": [ "proof3", "verify::proof2" ], "src/test.rs": [ "test::proof4", "test::proof5" ] }, "contract-harnesses": { "src/lib.rs": [ "proof" ] }, "contracts": [ { "function": "bar", "file": "src/lib.rs", "harnesses": [ "proof" ] } ], "totals": { "standard-harnesses": 4, "contract-harnesses": 1, "functions-under-contract": 1 } }"standard-harnesses"and"contract-harnesses"into an array calledALL_HARNESSESand the length of that array intoHARNESS_COUNT. (So in this example,ALL_HARNESSES = [proof3, verify::proof2, test::proof4, test::proof5, proof]andHARNESS_COUNT=5).proof3andverify::proof2, then we callkani verify-std --harness proof3 --harness verify::proof2 --exact. The--exactmakes Kani look for the exact harness name. This is important so that we don't match on partial patterns, e.g., if there is a harness called "foo" and a harness called "foo_bar", passing--harness foowithout--exactwould match against both harnesses, and thenfoo_barwould run twice.-jto Kani.I chose four workers somewhat arbitrarily--it makes each worker take about 45 minutes to an hour to finish. I thought it was good to have a balance between too few workers (which still makes us wait a while) and too many workers (which makes you look through more logs to find where a given harness is being verified). But happy to play with this number if people have opinions.
By submitting this pull request, I confirm that my contribution is made under the terms of the Apache 2.0 and MIT licenses.